Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    a__fib(N)  → a__sel(mark(N),a__fib1(s(0),s(0)))
2:    a__fib1(X,Y)  → cons(mark(X),fib1(Y,add(X,Y)))
3:    a__add(0,X)  → mark(X)
4:    a__add(s(X),Y)  → s(a__add(mark(X),mark(Y)))
5:    a__sel(0,cons(X,XS))  → mark(X)
6:    a__sel(s(N),cons(X,XS))  → a__sel(mark(N),mark(XS))
7:    mark(fib(X))  → a__fib(mark(X))
8:    mark(sel(X1,X2))  → a__sel(mark(X1),mark(X2))
9:    mark(fib1(X1,X2))  → a__fib1(mark(X1),mark(X2))
10:    mark(add(X1,X2))  → a__add(mark(X1),mark(X2))
11:    mark(s(X))  → s(mark(X))
12:    mark(0)  → 0
13:    mark(cons(X1,X2))  → cons(mark(X1),X2)
14:    a__fib(X)  → fib(X)
15:    a__sel(X1,X2)  → sel(X1,X2)
16:    a__fib1(X1,X2)  → fib1(X1,X2)
17:    a__add(X1,X2)  → add(X1,X2)
There are 25 dependency pairs:
18:    A__FIB(N)  → A__SEL(mark(N),a__fib1(s(0),s(0)))
19:    A__FIB(N)  → MARK(N)
20:    A__FIB(N)  → A__FIB1(s(0),s(0))
21:    A__FIB1(X,Y)  → MARK(X)
22:    A__ADD(0,X)  → MARK(X)
23:    A__ADD(s(X),Y)  → A__ADD(mark(X),mark(Y))
24:    A__ADD(s(X),Y)  → MARK(X)
25:    A__ADD(s(X),Y)  → MARK(Y)
26:    A__SEL(0,cons(X,XS))  → MARK(X)
27:    A__SEL(s(N),cons(X,XS))  → A__SEL(mark(N),mark(XS))
28:    A__SEL(s(N),cons(X,XS))  → MARK(N)
29:    A__SEL(s(N),cons(X,XS))  → MARK(XS)
30:    MARK(fib(X))  → A__FIB(mark(X))
31:    MARK(fib(X))  → MARK(X)
32:    MARK(sel(X1,X2))  → A__SEL(mark(X1),mark(X2))
33:    MARK(sel(X1,X2))  → MARK(X1)
34:    MARK(sel(X1,X2))  → MARK(X2)
35:    MARK(fib1(X1,X2))  → A__FIB1(mark(X1),mark(X2))
36:    MARK(fib1(X1,X2))  → MARK(X1)
37:    MARK(fib1(X1,X2))  → MARK(X2)
38:    MARK(add(X1,X2))  → A__ADD(mark(X1),mark(X2))
39:    MARK(add(X1,X2))  → MARK(X1)
40:    MARK(add(X1,X2))  → MARK(X2)
41:    MARK(s(X))  → MARK(X)
42:    MARK(cons(X1,X2))  → MARK(X1)
Consider the SCC {18-42}. The constraints could not be solved.
Tyrolean Termination Tool  (3.58 seconds)   ---  May 3, 2006